\section{Приближеное вычисление\\
неподвижных точек}

Будем считать, что нам нужна наименьшая неподвижная точка монотонной функции $f$ в полной решетке.
Она всегда есть, но её не всегда можно точно посчитать --- $f$ не обязана быть непрерывной,
высота не обязана быть конечной и пр.

Бинарная операция $\uparrow : L\to L\to L$ --- оператор верхней грани (\emph{upper bound operator}), если
$\forall x, y : y \sqsubseteq (x\uparrow y) \sqsupseteq x$ (то есть больше каждого из операндов).
Важно, что других требований нет (никакой ассоциативности, коммутативности и пр., это будет
использоваться).

Если есть последовательность $\{x_n\}$, то с помощью ``$\uparrow$'' можно по ней построить другую 
последовательность $\{x^\uparrow_n\}$ следующим образом:

$$
x^\uparrow_n=\left\{
              \begin{array}{rcl}
                 x_0&,&n=0\\
                 x^\uparrow_{n-1}\uparrow x_n&,&n>0
              \end{array}
           \right.
$$

Свойства: для любой $\{x_n\}$ последовательность $\{x^\uparrow_n\}$ --- возрастающая; для любого 
$n$ $x^\uparrow_n\sqsupseteq\bigsqcup\{x_0,\dots,x_n\}$

Оператор расширения (\emph{widening operator}) $\nabla : L\to L\to L$:

\begin{itemize}
\item $\nabla$ --- оператор верхней грани;
\item для произвольной возрастающей последовательности $\{x_n\}$ последовательность $\{x^\nabla_n\}$ ---
стабилизируется.
\end{itemize}

Как им пользоваться? Пусть у нас есть полная решетка и монотонная функция $f$. Итерирование $f$ от 
наименьшего элемента не обязано привести нас в $\lfp{f}$. Но если у нас есть оператор расширения
$\nabla$, то мы можем с его помоью по $f$ построить специальную последовательность $\{f^\nabla_n\}$
следующим образом:

$$
f^\nabla_n=\left\{
            \begin{array}{rcl}
              \bot&,&n=0\\
              f^\nabla_{n-1}&,& f(f^\nabla_{n-1})\sqsubseteq f^\nabla_{n-1}\\
              f^\nabla_{n-1}\nabla f(f^\nabla_{n-1})&,&\mbox{иначе}
            \end{array}
          \right.
$$

Комментарий: сие есть ``исправленная'' последовательность итераций от наименьшего элемента.
Поскольку эта последовательность отличается от последовательности итераций (которая возрастающая и,
поэтому, в каждой точке которой $f$ экстенсивна), то надо учесть, что иногда применение $f$ 
дает нам движение ``вниз'' (``против шерсти'') --- это обрабатывается случаем 2. А когда
функция экстенсивна в очередной точке, то все равно сам образ взять нельзя, так как не будет
гарантироваться стабилизация --- вместо этого этот образ ``смешивается'' оператором расширения
с предыдущей точкой.

Можно доказать, что $\{f^\nabla_n\}$ --- стабилизируется, мало того, она стабилизируется тогда,
когда $f$ становится редуктивной по очередной точке (и после этого уже ничего не меняется).
Кроме того, ``предельная'' точка $\bigsqcup\{f^\nabla_n\}\sqsupseteq\lfp{f}$ (см. Нильсена или
сам). Пример использования --- интервальный анализ.

Оператор расширения (если его удалось построить) всегда позволяет посчитать корректное (то есть
``сверху'') приближение к наименьшей неподвижной точке. Поскольку в на полученном приближении
$f$ редуктивна, можно это приближение улучшить, итерируя от него $f$ любое число раз.

Оператор сжатия (\emph{narrowing operator}) --- это бинарная операция $\delta : L\to L\to L$, 
такая, что:

\begin{itemize}
\item если $x\sqsubseteq y$, то 
\end{itemize}
